\begin{tabbing}
$\forall$\=$E$:Type\{i\}, $T$, $V$:(Id$\rightarrow$Id$\rightarrow$Type\{i\}), $M$:(IdLnk$\rightarrow$Id$\rightarrow$Type\{i\}), ${\it loc}$:($E$$\rightarrow$Id), ${\it kind}$:($E$$\rightarrow$Knd),\+
\\[0ex]${\it val}$:($e$:$E$$\rightarrow$eventtype(${\it kind}$;${\it loc}$;$V$;$M$;$e$)), ${\it when}$, ${\it after}$:($x$:Id$\rightarrow$$e$:$E$$\rightarrow\mathbb{Q}\rightarrow$$T$(${\it loc}$($e$),$x$)),
\\[0ex]${\it time}$:($E$$\rightarrow\mathbb{Q}$), ${\it sends}$:($l$:IdLnk$\rightarrow$$E$$\rightarrow$(Msg\_sub($l$;$M$) List)),
\\[0ex]${\it sender}$:(\{$e$:$E$$\mid$ $\uparrow$isrcv(${\it kind}$($e$))\} $\rightarrow$$E$),
\\[0ex]${\it index}$:($e$:\{$e$:$E$$\mid$ $\uparrow$isrcv(${\it kind}$($e$))\} $\rightarrow$\{0..$\parallel$${\it sends}$(lnk(${\it kind}$($e$)),${\it sender}$($e$))$\parallel^{-}$\}), ${\it first}$:($E$$\rightarrow\mathbb{B}$),
\\[0ex]${\it pred}$:(\{${\it e'}$:$E$$\mid$ $\neg$($\uparrow$(${\it first}$(${\it e'}$)))\} $\rightarrow$$E$), ${\it causl}$:($E$$\rightarrow$$E$$\rightarrow\mathbb{P}$\{i\}).
\-\\[0ex]ESAxioms\=\{i:l\}\+
\\[0ex](\=$E$;\+
\\[0ex]$T$;
\\[0ex]$M$;
\\[0ex]${\it loc}$;
\\[0ex]${\it kind}$;
\\[0ex]${\it val}$;
\\[0ex]${\it when}$;
\\[0ex]${\it after}$;
\\[0ex]${\it time}$;
\\[0ex]${\it sends}$;
\\[0ex]${\it sender}$;
\\[0ex]${\it index}$;
\\[0ex]${\it first}$;
\\[0ex]${\it pred}$;
\\[0ex]${\it causl}$)
\-\-\\[0ex]$\in$ $\mathbb{P}$\{i'\}
\end{tabbing}